\begin{tabbing}
$\forall$\=$T$:Type, $t$:$T$, $l$:IdLnk, ${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $Q$:(State(${\it ds}_{2}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$),\+
\\[0ex]$d_{1}$:($\forall$$s$:State(${\it ds}_{1}$). Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($\neg_{b}$($P$($s$,$n$)))))),
\\[0ex]$d_{2}$:($\forall$$s$:State(${\it ds}_{2}$). Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($\neg_{b}$($Q$($s$,$n$)))))), $f$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$$T$).
\-\\[0ex]Normal(${\it ds}_{1}$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}_{2}$)
\\[0ex]$\Rightarrow$ ($\neg$(destination($l$) = source($l$) $\in$ Id))
\\[0ex]$\Rightarrow$ R{-}Feasible(sendMinimalR\=\{a:ut2, tg:ut2\}\+
\\[0ex]($T$; $t$; $l$; ${\it ds}_{1}$; ${\it ds}_{2}$; $P$; $Q$; $d_{1}$; $d_{2}$; $f$))
\-
\end{tabbing}